| Definitions | t  T,  x:A. B(x), State(ds), x:A  B(x), S  T, State(ds), @i (with ds: ds action a:T precondition a(v) is P s v), es is an event system of D, ES, Type, {x:A| B(x) }, Prop, S  T, @i Precondition for a(v)P State(ds) (v:T),  x.A(x), P   Q,  x. t(x), Id, a:A fp B(a), D realizes es. P(es),  b, M.da(a), IdLnk, unsolvable M.pre(a,s), a declared in M, x:A B(x), P & Q, A & B, {T}, f(x), x dom(f), mk-ma, x : v, f(x)?z, z != f(x) P(a;z), (with ds: ds action a:T precondition a(v) is P s v), M.ds(x), M.bframe(k sends on l), M(i), M.aframe(k affects x), M.sframe(k sends <l,tg>), M.frame(k affects x), M.send(k;l;s;v;ms;i), M.ef(k,x,s,v,w), M.pre(a,s,v), M.init(x,v), PossibleWorld(D;w), E, es_info(es), kind(e), act(e), loc(e), es-V(es), tag(e), lnk(e), es-M(es), es_val(es), es-Trans(es), es_init(es), es-pred?(es), acttype(e), rcvtype(e), isrcv(e), es-T(es), ES(the_w), E, state after e, val(e), (state when e), valtype(e), vartype(i;x), FairFifo, World, D realizes2 es.P(es), true, IdDeq, eqof(d), f(a), s ~ t, vartype(i;x), <a,b>, Top, 2of(t), 1of(t), deq-member(eq;x;L), if b t else f fi, s = t,  ,  A, b, P  Q, Unit, left+right, type List, (x l), hd(l), P Q, False, locl(a), kind(e), Knd, loc(e), KindDeq, SQType(T), A B,  ,  , valtype(i;a), act(e), isnull(a), Void, Atom$n, Action(i), a(i;t), product-deq(A;B;a;b), w.TA, e@i. P(e), P  Q,  ee'.P(e'), x:A. B(x), time(e), #$n, a<b, act(k), tag(k), lnk(k), w.M, isrcv(k), True, islocal(k), val(a), val(e), state_when(e), w.T, V(i;k), kindcase(k; a.f(a); l,t.g(l;t) ), rcv(l,tg), e e' , n+m, (e < e'), (e <loc e'), w-info(w;e), loc(e), Dec(P), e < e', w-pred(w;e), kind(a), state_after(e), kind(e),  x:A. B(x), x,y. t(x;y), i j, -n, n-m,  T, i j < k, {i..j }, s(i;t).x |
| Lemmas | w-s wf, decidable ex int seg, decidable not, int seg wf, w-state-after, member wf, squash wf, true wf, w-stutter, w-kind wf, decidable le, decidable assert, ge wf, nat properties, fpf-val-single1, fpf-cap-single1, fpf-single-dom, loc wf, kind wf, w state after wf, cless wf, w-info wf, w-pred wf, decidable lt, w-cless-loc, pi1 wf, pi2 wf, nat wf, w-eval wf, w-state-when, w state when wf, subtype rel dep function, fpf-cap wf, subtype rel self, w-a-not-null, w-time wf, ifthenelse wf, isrcv wf, w-M wf, lnk wf, tagof wf, w-TA wf, actof wf, le wf, es-valtype-w-valtype, w-isnull wf, w-a wf, Id sq, Knd sq, Kind-deq wf, Knd wf, w-ekind wf, locl wf, w-loc wf, w-E wf, fpf-ap wf, not functionality wrt iff, assert-deq-member, l member wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, assert wf, top wf, fpf-dom wf, fpf-trivial-subtype-top, deq-member wf, w-vartype wf, world wf, fair-fifo wf, possible-world wf, eqof eq btrue, id-deq wf, w-loc-lemma, w-kind-lemma, fpf wf, Id wf, d-realizes2-implies-realizes, pre-p wf, decl-state wf, event system wf, d-es wf, d-single-pre wf, ma-state wf |